/* ==============================================================================
*
*   Copyright (c) 2010, Pierre Favier
*   All rights reserved.
*
*   NTasking is free software: you can redistribute it and/or modify it
*   under the terms of the GNU General Public License as published by the
*   Free Software Foundation.
*
*   Redistribution and use in source and binary forms, with or without
*   modification, are permitted provided that the following conditions
*   are met:
*
*   -   Redistributions of source code must retain the above copyright notice,
*       this list of conditions and the following disclaimer.
*
*   -   Redistributions in binary form must reproduce the above
*       copyright notice, this list of conditions and the following
*       disclaimer in the documentation and/or other materials
*       provided with the distribution.
*
*   THIS SOFTWARE IS PROVIDED "AS IS" AND ANY EXPRESS OR IMPLIED
*   WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
*   OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
*   DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS
*   BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
*   EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
*   TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
*   DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
*   ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR
*   TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF
*   THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
*   SUCH DAMAGE.
*
* ============================================================================== */

using System;
using NTasking.ValidationTests.ACATS_3_0.Support;
using NUnit.Framework;
using Rhino.Mocks;

namespace NTasking.ValidationTests.ACATS_3_0.C9
{

    [TestFixture(Description = "")]
    public class C940004 : ValidationTest
    {

        //      Declare a resource descriptor tagged type.  Extend the type and
        //      use the extended type in a protected data structure.
        //      Implement a binary semaphore type.  Declare an entry for
        //      requesting a specific resource and an procedure for releasing the
        //      same resource.  Declare an object of this (protected) type.
        //      Declare and start three tasks each of which asks for a resource
        //      when directed to.  Verify that resources are properly allocated
        //      and deallocated.


        private static Semaphore<UserDesc> printerAccessMgr;
        private static int TcTimesObtained = 0;
        private static int TcTimesReleased = 0;

        
        private class UserDescriptor
        {

            internal int Id { get; set; }


            internal UserDescriptor()
            {
                Id = 0;
            }

        }


        private class UserRec : UserDescriptor
        {

            internal bool AccessToResource { get; set; }


            internal UserRec()
            {
                AccessToResource = false;
            }

        }


        private class Semaphore<RecT> : Protected
            where RecT : UserRec
        {

            private bool inUse = false;


            [Entry]
            internal Func<RecT, RecT> Request { get; private set; }


            [ReadWriteOperation]
            internal Func<RecT, RecT> Release { get; private set; }


            [ReadOnlyOperation]
            internal Func<int> TcCount { get; private set; }


            public Semaphore()
            {
                // when granted, secures a resource
                Entry(Request,
                    When: () => !inUse,
                Is: user =>
                {
                    inUse = true;
                    user.AccessToResource = true;
                    return user;
                });


                // when called, releases a resource
                ReadWriteOperation(Release, Is: user =>
                {
                    inUse = false;
                    user.AccessToResource = false;
                    return user;
                });


                // returns number of available resources
                ReadOnlyOperation(TcCount, Is: () =>
                {
                    return Count(Request);
                });
            }

        }


        private class UserDesc : UserRec
        {

            internal int NewDetails { get; set; }


            internal UserDesc()
            {
                NewDetails = 0;
            }

        }


        private class UserTask : ValidationTestTask
        {

            private UserDesc D = new UserDesc();


            [Entry]
            internal Action GetPrinter { get; private set; }


            [Entry]
            internal Func<UserDesc, UserDesc> ReleasePrinter { get; private set; }


            [Entry]
            internal Func<UserDesc> TcGetDescriptor { get; private set; }


            internal UserTask(IValidationTestResult result, int id)
                : base(result)
            {
                D.Id = id;
            }


            protected override void Body()
            {
                bool finished = false;

                while (!finished)
                {
                    Select(s => s.

                        Accept(GetPrinter).
                        Then(() =>
                        {
                            // request resource; if resource is not available,
                            // task will be queued to wait
                            D = printerAccessMgr.Request(D);

                            //===================//
                            // Test management machinery
                            //===================//

                            // when request granted, note it and post a message
                            TcTimesObtained += 1;
                        }).

                    Or.

                        Accept(ReleasePrinter, data =>
                        {
                            // release the resource, note its release
                            D = printerAccessMgr.Release(D);
                            TcTimesReleased += 1;
                            return D;
                        }).
                        Then(() =>
                        {
                            finished = true;
                        }).

                    Or.

                        Accept(TcGetDescriptor, () =>
                        {
                            return D;
                        })
                    );
                }
            }
            protected override void Exception(Exception ex)
            {
                Console.WriteLine("exception raised in User_Task");
                Result.TestFailed();
            }
        }


        [Test(Description =
                "Check that a protected record can be used to control access to" +
                "resources (data internal to the protected record).")]
        public void Test()
        {
            IValidationTestResult result = Mocks.DynamicMock<IValidationTestResult>();
            UserTask task1 = null;
            UserTask task2 = null;
            UserTask task3 = null;
            UserDesc rec1 = new UserDesc();
            UserDesc rec2 = new UserDesc();
            UserDesc rec3 = new UserDesc();

            Ada.Declare(() =>
            {
                printerAccessMgr = new Semaphore<UserDesc>();

                TcTimesObtained = 0;
                TcTimesReleased = 0;

                task1 = new UserTask(result, 1);
                task2 = new UserTask(result, 2);
                task3 = new UserTask(result, 3);

                // Setup text expectations

                Expect.Call(result.TestFailed).Repeat.Never();
                Mocks.ReplayAll();
            },
            Begin: () =>
            {
                // Start test execution

                if (TcTimesObtained != 0 ||
                    TcTimesReleased != 0 ||
                    rec1.AccessToResource ||
                    rec2.AccessToResource ||
                    rec3.AccessToResource)
                {
                    Console.WriteLine("Wrong initial conditions");
                    result.TestFailed();
                }

                // ask for resource
                // request for resource should be granted
                task1.GetPrinter();

                // wait here 'til task gets resource
                rec1 = task1.TcGetDescriptor();

                if (TcTimesObtained != 1 ||
                    TcTimesReleased != 0 ||
                    !rec1.AccessToResource)
                {
                    Console.WriteLine("Resource not assigned to task 1");
                    result.TestFailed();
                }

                // ask for resource
                // request for resource should be denied and task queued to wait
                task2.GetPrinter();

                // Task 1 still waiting to accept Release_Printer, still holds resource
                // Task 2 queued on Semaphore.Request

                // Ensure that Task2 is queued before continuing to make checks and queue
                // Task3. We use a for loop here to avoid hangs in broken implementations.

                for (int i = 1 ; i <= 20 ; i++)
                {
                    if (printerAccessMgr.TcCount() >= 1)
                        break;

                    Ada.Delay(Impdef.MinimumTaskSwitch);
                }

                if (TcTimesObtained != 1 ||
                    TcTimesReleased != 0)
                {
                    Console.WriteLine("Resource assigned to task 2");
                    result.TestFailed();
                }

                // ask for resource
                // request for resource should be denied and task 3 queued on Semaphore.Request
                task3.GetPrinter();

                // task 1 releases resource
                // released resource should be given to queued task 2.
                rec1 = task1.ReleasePrinter(rec1);

                // wait here for task 2
                rec2 = task2.TcGetDescriptor();

                // Task 1 has released resource and completed
                // Task 2 has seized the resource
                // Task 3 is queued on Semaphore.Request

                if (TcTimesObtained != 2 ||
                    TcTimesReleased != 1 ||
                    rec1.AccessToResource ||
                    !rec2.AccessToResource)
                {
                    Console.WriteLine("Resource not properly released/assigned to task 2");
                    result.TestFailed();
                }

                // task 2 releases resource
                rec2 = task2.ReleasePrinter(rec2);

                // task 3 is released from queue, and is given resource

                // wait here for task 3
                rec3 = task3.TcGetDescriptor();

                if (TcTimesObtained != 3 ||
                    TcTimesReleased != 2 ||
                    rec2.AccessToResource ||
                    !rec3.AccessToResource)
                {
                    Console.WriteLine("Resource not properly released/assigned to task 3");
                    result.TestFailed();
                }

                // task 3 releases resource
                rec3 = task3.ReleasePrinter(rec2);

                if (TcTimesObtained != 3 ||
                    TcTimesReleased != 3 ||
                    rec3.AccessToResource)
                {
                    Console.WriteLine("Resource not properly released by task 3");
                    result.TestFailed();
                }

                while (!task1.Terminated || !task2.Terminated || !task3.Terminated)
                    Ada.Delay(Impdef.MinimumTaskSwitch);
            });
        }

    }

}
